∧I LISTINDUCTION1;
EVAL ∀v w.rev1(qNIL*v,w)=rev1(v,rev1(qNIL,w)) BY { APPEND_DEF,REV1_DEF};
ASSUME ∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w));
∀E APPEND_DEF uu,v;
REWRITE ↑ BY LOGICTREE∪SEXPSS;
REWRITE rev1(uu*v,w) BY { 19};
∀E REV1_DEF cons(car uu,cdr uu*v),w;
REWRITE ↑ BY LOGICTREE∪SEXPSS;
REWRITE ↑↑↑ BY { 22};
∀I ↑ uu;
REWRITE ↑↑ BY { H_DIS};
∀E REV1_DEF uu,w;
REWRITE ↑ BY SEXPSS∪LOGICTREE;
TAUTEQ rev1(cdr uu,cons(car uu,w))=rev1(uu,w) 27;
REWRITE 25 BY { 28};
∀I ↑ v w;
⊃I H_DIS⊃↑;
∀I ↑ uu;
TAUT ∀u v w.rev1(u*v,w)=rev1(v,rev1(u,w)) I_DIS:NIL_DIS,32;